a,b:atom. (a = b)  (eq_atom(a; b)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, prop{i:l}, P  Q, t  T, x. t(x), P  Q, x(s)
Lemmas	all functionality wrt iff, iff wf, assert wf, eq atom wf, iff functionality wrt iff, assert of eq atom